COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Formal reasoning
C00006 ENDMK
C⊗;
Formal reasoning

	Our work in formal reasoning comes from two sources.  The first
is in artificial intelligence itself, and the second comes from our
other goal of verifying the correctness of computer programs.

	In order to make a computer carry out reasoning, we should
understand reasoning as precisely as possible.  A big step in understanding
reasoning was made about 75 years ago with the invention of %2first order
logic%1 and %2axiomatic set theory%1.  In these mathematical languages, one
can make statements about any subject matter in terms of some properties
and relations that are taken as basic for that subject.  The idea of
logical consequence is so precisely defined for these systems that a
computer program can tell whether a statement follows directly from one
or two others, and likewise a computer program can check a long chain
of reasoning in which each statement must either be identified as an
assumption or must follow directly from preceding statements.
Shortly after the invention of these logical systems, it was shown in
principle how all mathematical reasoning could be expressed in them,
but it was understood that the proofs would be very long compared to
usual informal mathematical proofs so that the formal logical systems were not
actually used for communication among mathematicians.  
Instead they were used for reasoning about mathematical reasoning itself
which is called %2metamathematics%1.

	When computers came along in the 1950s, interest in actually using
first order logic revived.  Programs came along for proving
statements from assumptions, and it was hoped that one could base
artificial intelligence on programs that solved problems by proving a
solution existed and finding it as a by-product of the proof.
In the 1960s, a number of such programs were written, and some
success was achieved, especially in some areas of mathematics where
human intuition is weak, but problems arose in getting a generally
applicable program, and this is where our research
comes in.

	1. The knowledge provided to the programs is divided into a
general knowledge part and a part specific to the problem being
solved.  However, it often turned out that what was supposed to be
general knowledge was not usable in other problems, i.e. it was
really ad hoc.

	2.